Separation logic

In computer science, separation logic[1] is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang,[1][2][3][4] drawing upon early work by Burstall.[5] The assertion language of separation logic is a special case of the logic of bunched implications (BI).[6]

Separation logic facilitates reasoning about:

Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm checks the validity of another algorithm) and automated parallelization of software.

Contents

Assertions: Operators and semantics

Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack-allocated) variables and dynamically-allocated objects in common programming languages such as C and Java. A store s is a function mapping variables to values. A heap h is a partial function mapping memory addresses to values. Two heaps h and h' are disjoint (denoted h \bot h') if their domains do not overlap (i.e., if for every memory address \ell, at least one of h(\ell) and h'(\ell) is undefined).

The logic allows to prove judgements of the form s, h \models P, where s is a store, h is a heap, and P is an assertion over the given store and heap. Separation logic assertions (denoted as P, Q, R) contain the standard boolean connectives and, in addition, emp, e \mapsto e', P \ast Q, and P {-\!\!\ast} Q, where e and e' as expressions.

The operators \ast and -\!\!\ast share some properties in common with the classical conjunction and implication operators. They can be combined using an inference rule similar to modus ponens

\frac{s, h \models P \ast (P -\!\!\ast Q)}{s, h \models Q}

and they form an adjunction, i.e., s, h \cup h' \models P \ast Q \Rightarrow R if and only if s, h \models P \Rightarrow Q -\!\!\ast R for h \bot h'; more precisely, the adjoint operators are \_ \ast Q and Q -\!\!\ast \_.

Reasoning about programs: triples & proof rules

In separation logic, Hoare triples have a slightly different meaning than in Hoare logic. The triple \{P\}\ C\ \{Q\} asserts that if the program, C, executes from an initial state satisfying the precondition, P, then the program will not go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition, Q. In essence, during its execution, C may access only memory locations whose existence is asserted in the precondition or that have been allocated by C itself.

In addition to the standard rules from Hoare logic, separation logic supports the following very important rule:

\frac{ \{P\}\ C\ \{Q\} }{ \{P \ast R\}\ C\ \{Q \ast R\} }~\mathsf{mod}(C) \cap \mathsf{fv}(R) =\emptyset

This is known as the frame rule and enables local reasoning. It says that a program that executes safely in a small state (satisfying P), can also execute in any bigger state (satisfying P \ast R) and that its execution will not affect the additional part of the state (and so R will remain true in the postcondition).

Implementations

The Ynot library for the Coq proof assistant contains an implementation.

References

  1. ^ a b Separation Logic: A Logic for Shared Mutable Data Structures. John C. Reynolds. LICS 2002.
  2. ^ Intuitionistic Reasoning about Shared Mutable Data Structure. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare
  3. ^ BI as an Assertion Language for Mutable Data Structures. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
  4. ^ Local Reasoning about Programs that Alter Data Structures. Peter O'Hearn, John Reynolds, Hongseok Yang. CSL 2001
  5. ^ Some techniques for proving programs which alter data structures. R.M. Burstall. Machine Intelligence 7, 1972.
  6. ^ The Logic of Bunched Implications P.W. O'Hearn and D. J. Pym. Bulletin of Symbolic Logic , 5(2), June 1999, pp215-244